<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="common/css/sf.css" rel="stylesheet" type="text/css" />
<title>ImpParser: Lexing and Parsing in Coq</title>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/lf.css" rel="stylesheet" type="text/css"/>
</head>

<body>

<div id="page">

<div id="header">
<div id='logoinheader'><a href='https://softwarefoundations.cis.upenn.edu'>
<img src='common/media/image/sf_logo_sm.png' alt='Software Foundations Logo'></a></div>
<div class='booktitleinheader'><a href='index.html'>Volume 1: Logical Foundations</a></div>
<ul id='menu'>
   <li class='section_name'><a href='toc.html'>Table of Contents</a></li>
   <li class='section_name'><a href='coqindex.html'>Index</a></li>
   <li class='section_name'><a href='deps.html'>Roadmap</a></li>
</ul>
</div>

<div id="main">

<h1 class="libtitle">ImpParser<span class="subtitle">Lexing and Parsing in Coq</span></h1>


<div class="doc">

<div class="paragraph"> </div>

 The development of the Imp language in <span class="inlinecode"><span class="id" title="var">Imp.v</span></span> completely ignores
    issues of concrete syntax -- how an ascii string that a programmer
    might write gets translated into abstract syntax trees defined by
    the datatypes <span class="inlinecode"><span class="id" title="var">aexp</span></span>, <span class="inlinecode"><span class="id" title="var">bexp</span></span>, and <span class="inlinecode"><span class="id" title="var">com</span></span>.  In this chapter, we
    illustrate how the rest of the story can be filled in by building
    a simple lexical analyzer and parser using Coq's functional
    programming facilities. 
<div class="paragraph"> </div>

 It is not important to understand all the details here (and
    accordingly, the explanations are fairly terse and there are no
    exercises).  The main point is simply to demonstrate that it can
    be done.  You are invited to look through the code -- most of it
    is not very complicated, though the parser relies on some
    "monadic" programming idioms that may require a little work to
    make out -- but most readers will probably want to just skim down
    to the Examples section at the very end to get the punchline. 
</div>
<div class="code">

<span class="id" title="keyword">Set</span> <span class="id" title="var">Warnings</span> "-notation-overridden,-parsing,-deprecated-hint-without-locality".<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#"><span class="id" title="library">Strings.String</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.Ascii.html#"><span class="id" title="library">Strings.Ascii</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Arith.Arith.html#"><span class="id" title="library">Arith.Arith</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Nat.html#"><span class="id" title="library">Init.Nat</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Arith.EqNat.html#"><span class="id" title="library">Arith.EqNat</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#"><span class="id" title="library">Lists.List</span></a>. <span class="id" title="keyword">Import</span> <span class="id" title="var">ListNotations</span>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">LF</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Maps.html#"><span class="id" title="library">Maps</span></a> <a class="idref" href="Imp.html#"><span class="id" title="library">Imp</span></a>.<br/>
</div>

<div class="doc">
<a id="lab384"></a><h1 class="section">Internals</h1>

</div>

<div class="doc">
<a id="lab385"></a><h2 class="section">Lexical Analysis</h2>

</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="isWhite" class="idref" href="#isWhite"><span class="id" title="definition">isWhite</span></a> (<a id="c:1" class="idref" href="#c:1"><span class="id" title="binder">c</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.Ascii.html#ascii"><span class="id" title="inductive">ascii</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">let</span> <a id="n:2" class="idref" href="#n:2"><span class="id" title="binder">n</span></a> := <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.Ascii.html#nat_of_ascii"><span class="id" title="definition">nat_of_ascii</span></a> <a class="idref" href="ImpParser.html#c:1"><span class="id" title="variable">c</span></a> <span class="id" title="keyword">in</span><br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#orb"><span class="id" title="definition">orb</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#orb"><span class="id" title="definition">orb</span></a> (<a class="idref" href="ImpParser.html#n:2"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Nat.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> 32)   <span class="comment">(*&nbsp;space&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="ImpParser.html#n:2"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Nat.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> 9))   <span class="comment">(*&nbsp;tab&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#orb"><span class="id" title="definition">orb</span></a> (<a class="idref" href="ImpParser.html#n:2"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Nat.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> 10)   <span class="comment">(*&nbsp;linefeed&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="ImpParser.html#n:2"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Nat.html#ad2ec4e405f68c46c0a176e3e94ae2e<sub>3</sub>"><span class="id" title="notation">=?</span></a> 13)). <span class="comment">(*&nbsp;Carriage&nbsp;return.&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Notation</span> <a id="0f31f5c1c6b6a21a3a187247222bc9e<sub>4</sub>" class="idref" href="#0f31f5c1c6b6a21a3a187247222bc9e<sub>4</sub>"><span class="id" title="notation">&quot;</span></a>x '&lt;=?' y" := (<span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Nat.html#0f31f5c1c6b6a21a3a187247222bc9e<sub>4</sub>"><span class="id" title="notation">&lt;=?</span></a> <span class="id" title="var">y</span>)<br/>
&nbsp;&nbsp;(<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 70, <span class="id" title="keyword">no</span> <span class="id" title="keyword">associativity</span>) : <span class="id" title="var">nat_scope</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="isLowerAlpha" class="idref" href="#isLowerAlpha"><span class="id" title="definition">isLowerAlpha</span></a> (<a id="c:3" class="idref" href="#c:3"><span class="id" title="binder">c</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.Ascii.html#ascii"><span class="id" title="inductive">ascii</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">let</span> <a id="n:4" class="idref" href="#n:4"><span class="id" title="binder">n</span></a> := <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.Ascii.html#nat_of_ascii"><span class="id" title="definition">nat_of_ascii</span></a> <a class="idref" href="ImpParser.html#c:3"><span class="id" title="variable">c</span></a> <span class="id" title="keyword">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#andb"><span class="id" title="definition">andb</span></a> (97 <a class="idref" href="ImpParser.html#0f31f5c1c6b6a21a3a187247222bc9e<sub>4</sub>"><span class="id" title="notation">&lt;=?</span></a> <a class="idref" href="ImpParser.html#n:4"><span class="id" title="variable">n</span></a>) (<a class="idref" href="ImpParser.html#n:4"><span class="id" title="variable">n</span></a> <a class="idref" href="ImpParser.html#0f31f5c1c6b6a21a3a187247222bc9e<sub>4</sub>"><span class="id" title="notation">&lt;=?</span></a> 122).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="isAlpha" class="idref" href="#isAlpha"><span class="id" title="definition">isAlpha</span></a> (<a id="c:5" class="idref" href="#c:5"><span class="id" title="binder">c</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.Ascii.html#ascii"><span class="id" title="inductive">ascii</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">let</span> <a id="n:6" class="idref" href="#n:6"><span class="id" title="binder">n</span></a> := <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.Ascii.html#nat_of_ascii"><span class="id" title="definition">nat_of_ascii</span></a> <a class="idref" href="ImpParser.html#c:5"><span class="id" title="variable">c</span></a> <span class="id" title="keyword">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#orb"><span class="id" title="definition">orb</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#andb"><span class="id" title="definition">andb</span></a> (65 <a class="idref" href="ImpParser.html#0f31f5c1c6b6a21a3a187247222bc9e<sub>4</sub>"><span class="id" title="notation">&lt;=?</span></a> <a class="idref" href="ImpParser.html#n:6"><span class="id" title="variable">n</span></a>) (<a class="idref" href="ImpParser.html#n:6"><span class="id" title="variable">n</span></a> <a class="idref" href="ImpParser.html#0f31f5c1c6b6a21a3a187247222bc9e<sub>4</sub>"><span class="id" title="notation">&lt;=?</span></a> 90))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#andb"><span class="id" title="definition">andb</span></a> (97 <a class="idref" href="ImpParser.html#0f31f5c1c6b6a21a3a187247222bc9e<sub>4</sub>"><span class="id" title="notation">&lt;=?</span></a> <a class="idref" href="ImpParser.html#n:6"><span class="id" title="variable">n</span></a>) (<a class="idref" href="ImpParser.html#n:6"><span class="id" title="variable">n</span></a> <a class="idref" href="ImpParser.html#0f31f5c1c6b6a21a3a187247222bc9e<sub>4</sub>"><span class="id" title="notation">&lt;=?</span></a> 122)).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="isDigit" class="idref" href="#isDigit"><span class="id" title="definition">isDigit</span></a> (<a id="c:7" class="idref" href="#c:7"><span class="id" title="binder">c</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.Ascii.html#ascii"><span class="id" title="inductive">ascii</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">let</span> <a id="n:8" class="idref" href="#n:8"><span class="id" title="binder">n</span></a> := <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.Ascii.html#nat_of_ascii"><span class="id" title="definition">nat_of_ascii</span></a> <a class="idref" href="ImpParser.html#c:7"><span class="id" title="variable">c</span></a> <span class="id" title="keyword">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#andb"><span class="id" title="definition">andb</span></a> (48 <a class="idref" href="ImpParser.html#0f31f5c1c6b6a21a3a187247222bc9e<sub>4</sub>"><span class="id" title="notation">&lt;=?</span></a> <a class="idref" href="ImpParser.html#n:8"><span class="id" title="variable">n</span></a>) (<a class="idref" href="ImpParser.html#n:8"><span class="id" title="variable">n</span></a> <a class="idref" href="ImpParser.html#0f31f5c1c6b6a21a3a187247222bc9e<sub>4</sub>"><span class="id" title="notation">&lt;=?</span></a> 57).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Inductive</span> <a id="chartype" class="idref" href="#chartype"><span class="id" title="inductive">chartype</span></a> := <a id="white" class="idref" href="#white"><span class="id" title="constructor">white</span></a> | <a id="alpha" class="idref" href="#alpha"><span class="id" title="constructor">alpha</span></a> | <a id="digit" class="idref" href="#digit"><span class="id" title="constructor">digit</span></a> | <a id="other" class="idref" href="#other"><span class="id" title="constructor">other</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="classifyChar" class="idref" href="#classifyChar"><span class="id" title="definition">classifyChar</span></a> (<a id="c:11" class="idref" href="#c:11"><span class="id" title="binder">c</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.Ascii.html#ascii"><span class="id" title="inductive">ascii</span></a>) : <a class="idref" href="ImpParser.html#chartype"><span class="id" title="inductive">chartype</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="ImpParser.html#isWhite"><span class="id" title="definition">isWhite</span></a> <a class="idref" href="ImpParser.html#c:11"><span class="id" title="variable">c</span></a> <span class="id" title="keyword">then</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#white"><span class="id" title="constructor">white</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">else</span> <span class="id" title="keyword">if</span> <a class="idref" href="ImpParser.html#isAlpha"><span class="id" title="definition">isAlpha</span></a> <a class="idref" href="ImpParser.html#c:11"><span class="id" title="variable">c</span></a> <span class="id" title="keyword">then</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#alpha"><span class="id" title="constructor">alpha</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">else</span> <span class="id" title="keyword">if</span> <a class="idref" href="ImpParser.html#isDigit"><span class="id" title="definition">isDigit</span></a> <a class="idref" href="ImpParser.html#c:11"><span class="id" title="variable">c</span></a> <span class="id" title="keyword">then</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#digit"><span class="id" title="constructor">digit</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">else</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#other"><span class="id" title="constructor">other</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Fixpoint</span> <a id="list_of_string" class="idref" href="#list_of_string"><span class="id" title="definition">list_of_string</span></a> (<a id="s:12" class="idref" href="#s:12"><span class="id" title="binder">s</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.Ascii.html#ascii"><span class="id" title="inductive">ascii</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="ImpParser.html#s:12"><span class="id" title="variable">s</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#EmptyString"><span class="id" title="constructor">EmptyString</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#ae9a5e1034e143b218b09d8e454472bd"><span class="id" title="notation">[]</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#String"><span class="id" title="constructor">String</span></a> <span class="id" title="var">c</span> <span class="id" title="var">s</span> ⇒ <span class="id" title="var">c</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">(</span></a><a class="idref" href="ImpParser.html#list_of_string:13"><span class="id" title="definition">list_of_string</span></a> <a class="idref" href="ImpParser.html#s:12"><span class="id" title="variable">s</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="string_of_list" class="idref" href="#string_of_list"><span class="id" title="definition">string_of_list</span></a> (<a id="xs:15" class="idref" href="#xs:15"><span class="id" title="binder">xs</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.Ascii.html#ascii"><span class="id" title="inductive">ascii</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a> :=<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#fold_right"><span class="id" title="definition">fold_right</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#String"><span class="id" title="constructor">String</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#EmptyString"><span class="id" title="constructor">EmptyString</span></a> <a class="idref" href="ImpParser.html#xs:15"><span class="id" title="variable">xs</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="token" class="idref" href="#token"><span class="id" title="definition">token</span></a> := <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Fixpoint</span> <a id="tokenize_helper" class="idref" href="#tokenize_helper"><span class="id" title="definition">tokenize_helper</span></a> (<a id="cls:16" class="idref" href="#cls:16"><span class="id" title="binder">cls</span></a> : <a class="idref" href="ImpParser.html#chartype"><span class="id" title="inductive">chartype</span></a>) (<a id="acc:17" class="idref" href="#acc:17"><span class="id" title="binder">acc</span></a> <a id="xs:18" class="idref" href="#xs:18"><span class="id" title="binder">xs</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.Ascii.html#ascii"><span class="id" title="inductive">ascii</span></a>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.Ascii.html#ascii"><span class="id" title="inductive">ascii</span></a>) :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">let</span> <a id="tk:21" class="idref" href="#tk:21"><span class="id" title="binder">tk</span></a> := <span class="id" title="keyword">match</span> <a class="idref" href="ImpParser.html#acc:17"><span class="id" title="variable">acc</span></a> <span class="id" title="keyword">with</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#ae9a5e1034e143b218b09d8e454472bd"><span class="id" title="notation">[]</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#ae9a5e1034e143b218b09d8e454472bd"><span class="id" title="notation">[]</span></a> | <span class="id" title="var">_</span><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a><span class="id" title="var">_</span> ⇒ <a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#ddd65c2f7ee73ecec433744948d846bb"><span class="id" title="notation">[</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#rev"><span class="id" title="definition">rev</span></a> <a class="idref" href="ImpParser.html#acc:17"><span class="id" title="variable">acc</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#ddd65c2f7ee73ecec433744948d846bb"><span class="id" title="notation">]</span></a> <span class="id" title="keyword">end</span> <span class="id" title="keyword">in</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="ImpParser.html#xs:18"><span class="id" title="variable">xs</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#ae9a5e1034e143b218b09d8e454472bd"><span class="id" title="notation">[]</span></a> ⇒ <a class="idref" href="ImpParser.html#tk:21"><span class="id" title="variable">tk</span></a><br/>
&nbsp;&nbsp;| (<span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a><span class="id" title="var">xs'</span>) ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="ImpParser.html#cls:16"><span class="id" title="variable">cls</span></a>, <a class="idref" href="ImpParser.html#classifyChar"><span class="id" title="definition">classifyChar</span></a> <span class="id" title="var">x</span>, <span class="id" title="var">x</span> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">_</span>, <span class="id" title="var">_</span>, "("      ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#tk:21"><span class="id" title="variable">tk</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#bc347c51eaf667706ae54503b26d52c<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#ddd65c2f7ee73ecec433744948d846bb"><span class="id" title="notation">[</span></a>"("<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#ddd65c2f7ee73ecec433744948d846bb"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::(</span></a><a class="idref" href="ImpParser.html#tokenize_helper:19"><span class="id" title="definition">tokenize_helper</span></a> <a class="idref" href="ImpParser.html#other"><span class="id" title="constructor">other</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#ae9a5e1034e143b218b09d8e454472bd"><span class="id" title="notation">[]</span></a> <span class="id" title="var">xs'</span><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">_</span>, <span class="id" title="var">_</span>, ")"      ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#tk:21"><span class="id" title="variable">tk</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#bc347c51eaf667706ae54503b26d52c<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#ddd65c2f7ee73ecec433744948d846bb"><span class="id" title="notation">[</span></a>")"<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#ddd65c2f7ee73ecec433744948d846bb"><span class="id" title="notation">]</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::(</span></a><a class="idref" href="ImpParser.html#tokenize_helper:19"><span class="id" title="definition">tokenize_helper</span></a> <a class="idref" href="ImpParser.html#other"><span class="id" title="constructor">other</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#ae9a5e1034e143b218b09d8e454472bd"><span class="id" title="notation">[]</span></a> <span class="id" title="var">xs'</span><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">_</span>, <a class="idref" href="ImpParser.html#white"><span class="id" title="constructor">white</span></a>, <span class="id" title="var">_</span>    ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#tk:21"><span class="id" title="variable">tk</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#bc347c51eaf667706ae54503b26d52c<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#bc347c51eaf667706ae54503b26d52c<sub>6</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="ImpParser.html#tokenize_helper:19"><span class="id" title="definition">tokenize_helper</span></a> <a class="idref" href="ImpParser.html#white"><span class="id" title="constructor">white</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#ae9a5e1034e143b218b09d8e454472bd"><span class="id" title="notation">[]</span></a> <span class="id" title="var">xs'</span><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#bc347c51eaf667706ae54503b26d52c<sub>6</sub>"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="ImpParser.html#alpha"><span class="id" title="constructor">alpha</span></a>,<a class="idref" href="ImpParser.html#alpha"><span class="id" title="constructor">alpha</span></a>,<span class="id" title="var">x</span>  ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#tokenize_helper:19"><span class="id" title="definition">tokenize_helper</span></a> <a class="idref" href="ImpParser.html#alpha"><span class="id" title="constructor">alpha</span></a> (<span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a><a class="idref" href="ImpParser.html#acc:17"><span class="id" title="variable">acc</span></a>) <span class="id" title="var">xs'</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="ImpParser.html#digit"><span class="id" title="constructor">digit</span></a>,<a class="idref" href="ImpParser.html#digit"><span class="id" title="constructor">digit</span></a>,<span class="id" title="var">x</span>  ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#tokenize_helper:19"><span class="id" title="definition">tokenize_helper</span></a> <a class="idref" href="ImpParser.html#digit"><span class="id" title="constructor">digit</span></a> (<span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a><a class="idref" href="ImpParser.html#acc:17"><span class="id" title="variable">acc</span></a>) <span class="id" title="var">xs'</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="ImpParser.html#other"><span class="id" title="constructor">other</span></a>,<a class="idref" href="ImpParser.html#other"><span class="id" title="constructor">other</span></a>,<span class="id" title="var">x</span>  ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#tokenize_helper:19"><span class="id" title="definition">tokenize_helper</span></a> <a class="idref" href="ImpParser.html#other"><span class="id" title="constructor">other</span></a> (<span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a><a class="idref" href="ImpParser.html#acc:17"><span class="id" title="variable">acc</span></a>) <span class="id" title="var">xs'</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">_</span>,<span class="id" title="var">tp</span>,<span class="id" title="var">x</span>         ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#tk:21"><span class="id" title="variable">tk</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#bc347c51eaf667706ae54503b26d52c<sub>6</sub>"><span class="id" title="notation">++</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#bc347c51eaf667706ae54503b26d52c<sub>6</sub>"><span class="id" title="notation">(</span></a><a class="idref" href="ImpParser.html#tokenize_helper:19"><span class="id" title="definition">tokenize_helper</span></a> <span class="id" title="var">tp</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#ddd65c2f7ee73ecec433744948d846bb"><span class="id" title="notation">[</span></a><span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#ddd65c2f7ee73ecec433744948d846bb"><span class="id" title="notation">]</span></a> <span class="id" title="var">xs'</span><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#bc347c51eaf667706ae54503b26d52c<sub>6</sub>"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span> %<span class="id" title="var">char</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="tokenize" class="idref" href="#tokenize"><span class="id" title="definition">tokenize</span></a> (<a id="s:25" class="idref" href="#s:25"><span class="id" title="binder">s</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a> :=<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#map"><span class="id" title="definition">map</span></a> <a class="idref" href="ImpParser.html#string_of_list"><span class="id" title="definition">string_of_list</span></a> (<a class="idref" href="ImpParser.html#tokenize_helper"><span class="id" title="definition">tokenize_helper</span></a> <a class="idref" href="ImpParser.html#white"><span class="id" title="constructor">white</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#ae9a5e1034e143b218b09d8e454472bd"><span class="id" title="notation">[]</span></a> (<a class="idref" href="ImpParser.html#list_of_string"><span class="id" title="definition">list_of_string</span></a> <a class="idref" href="ImpParser.html#s:25"><span class="id" title="variable">s</span></a>)).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="tokenize_ex<sub>1</sub>" class="idref" href="#tokenize_ex<sub>1</sub>"><span class="id" title="definition">tokenize_ex<sub>1</sub></span></a> :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#tokenize"><span class="id" title="definition">tokenize</span></a> "abc12=3  223*(3+(a+c))" %<span class="id" title="var">string</span><br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">[</span></a>"abc"<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> "12"<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> "="<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> "3"<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> "223"<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"*"<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> "("<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> "3"<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> "+"<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> "("<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"a"<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> "+"<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> "c"<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> ")"<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">;</span></a> ")"<a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#e76c6291366b599375c28eba0aae94bb"><span class="id" title="notation">]</span></a>%<span class="id" title="var">string</span>.<br/>
<div class="togglescript" id="proofcontrol1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')"><span class="show"></span></div>
<div class="proofscript" id="proof1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')">
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
<a id="lab386"></a><h2 class="section">Parsing</h2>

<div class="paragraph"> </div>

<a id="lab387"></a><h3 class="section">Options With Errors</h3>

<div class="paragraph"> </div>

 An <span class="inlinecode"><span class="id" title="var">option</span></span> type with error messages: 
</div>
<div class="code">

<span class="id" title="keyword">Inductive</span> <a id="optionE" class="idref" href="#optionE"><span class="id" title="inductive">optionE</span></a> (<a id="X:26" class="idref" href="#X:26"><span class="id" title="binder">X</span></a>:<span class="id" title="keyword">Type</span>) : <span class="id" title="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <a id="SomeE" class="idref" href="#SomeE"><span class="id" title="constructor">SomeE</span></a> (<a id="x:29" class="idref" href="#x:29"><span class="id" title="binder">x</span></a> : <a class="idref" href="ImpParser.html#X:26"><span class="id" title="variable">X</span></a>)<br/>
&nbsp;&nbsp;| <a id="NoneE" class="idref" href="#NoneE"><span class="id" title="constructor">NoneE</span></a> (<a id="s:30" class="idref" href="#s:30"><span class="id" title="binder">s</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>).<br/><hr class='doublespaceincode'/>
<span class="id" title="var">Arguments</span> <a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> {<span class="id" title="var">X</span>}.<br/>
<span class="id" title="var">Arguments</span> <a class="idref" href="ImpParser.html#NoneE"><span class="id" title="constructor">NoneE</span></a> {<span class="id" title="var">X</span>}.<br/>
</div>

<div class="doc">
Some syntactic sugar to make writing nested match-expressions on
    optionE more convenient. 
</div>
<div class="code">

<span class="id" title="keyword">Notation</span> <a id="c2b4d6f0daa4552d70137fd9d8530127" class="idref" href="#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">&quot;</span></a>' p &lt;- e<sub>1</sub> ;; e<sub>2</sub>"<br/>
&nbsp;&nbsp;&nbsp;:= (<span class="id" title="keyword">match</span> <span class="id" title="var">e<sub>1</sub></span> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <span class="id" title="var">p</span> ⇒ <span class="id" title="var">e<sub>2</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="ImpParser.html#NoneE"><span class="id" title="constructor">NoneE</span></a> <span class="id" title="var">err</span> ⇒ <a class="idref" href="ImpParser.html#NoneE"><span class="id" title="constructor">NoneE</span></a> <span class="id" title="var">err</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span>)<br/>
&nbsp;&nbsp;&nbsp;(<span class="id" title="tactic">right</span> <span class="id" title="keyword">associativity</span>, <span class="id" title="var">p</span> <span class="id" title="tactic">pattern</span>, <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60, <span class="id" title="var">e<sub>1</sub></span> <span class="id" title="tactic">at</span> <span class="id" title="var">next</span> <span class="id" title="keyword">level</span>).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Notation</span> <a id="d3681d6f57c7eee49c36b58445e43f<sub>11</sub>" class="idref" href="#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">&quot;</span></a>'TRY' ' p &lt;- e<sub>1</sub> ;; e<sub>2</sub> 'OR' e<sub>3</sub>"<br/>
&nbsp;&nbsp;&nbsp;:= (<span class="id" title="keyword">match</span> <span class="id" title="var">e<sub>1</sub></span> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <span class="id" title="var">p</span> ⇒ <span class="id" title="var">e<sub>2</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="ImpParser.html#NoneE"><span class="id" title="constructor">NoneE</span></a> <span class="id" title="var">_</span> ⇒ <span class="id" title="var">e<sub>3</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span>)<br/>
&nbsp;&nbsp;&nbsp;(<span class="id" title="tactic">right</span> <span class="id" title="keyword">associativity</span>, <span class="id" title="var">p</span> <span class="id" title="tactic">pattern</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60, <span class="id" title="var">e<sub>1</sub></span> <span class="id" title="tactic">at</span> <span class="id" title="var">next</span> <span class="id" title="keyword">level</span>, <span class="id" title="var">e<sub>2</sub></span> <span class="id" title="tactic">at</span> <span class="id" title="var">next</span> <span class="id" title="keyword">level</span>).<br/>
</div>

<div class="doc">
<a id="lab388"></a><h3 class="section">Generic Combinators for Building Parsers</h3>

</div>
<div class="code">

<span class="id" title="keyword">Open</span> <span class="id" title="keyword">Scope</span> <span class="id" title="var">string_scope</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="parser" class="idref" href="#parser"><span class="id" title="definition">parser</span></a> (<a id="T:31" class="idref" href="#T:31"><span class="id" title="binder">T</span></a> : <span class="id" title="keyword">Type</span>) :=<br/>
&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="ImpParser.html#token"><span class="id" title="definition">token</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="ImpParser.html#optionE"><span class="id" title="inductive">optionE</span></a> (<a class="idref" href="ImpParser.html#T:31"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="ImpParser.html#token"><span class="id" title="definition">token</span></a>).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Fixpoint</span> <a id="many_helper" class="idref" href="#many_helper"><span class="id" title="definition">many_helper</span></a> {<a id="T:32" class="idref" href="#T:32"><span class="id" title="binder">T</span></a>} (<a id="p:33" class="idref" href="#p:33"><span class="id" title="binder">p</span></a> : <a class="idref" href="ImpParser.html#parser"><span class="id" title="definition">parser</span></a> <a class="idref" href="ImpParser.html#T:32"><span class="id" title="variable">T</span></a>) <a id="acc:34" class="idref" href="#acc:34"><span class="id" title="binder">acc</span></a> <a id="steps:35" class="idref" href="#steps:35"><span class="id" title="binder">steps</span></a> <a id="xs:36" class="idref" href="#xs:36"><span class="id" title="binder">xs</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="ImpParser.html#steps:35"><span class="id" title="variable">steps</span></a>, <a class="idref" href="ImpParser.html#p:33"><span class="id" title="variable">p</span></a> <a class="idref" href="ImpParser.html#xs:36"><span class="id" title="variable">xs</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| 0, <span class="id" title="var">_</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#NoneE"><span class="id" title="constructor">NoneE</span></a> "Too many recursive calls"<br/>
&nbsp;&nbsp;| <span class="id" title="var">_</span>, <a class="idref" href="ImpParser.html#NoneE"><span class="id" title="constructor">NoneE</span></a> <span class="id" title="var">_</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">((</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#rev"><span class="id" title="definition">rev</span></a> <a class="idref" href="ImpParser.html#acc:34"><span class="id" title="variable">acc</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">),</span></a> <a class="idref" href="ImpParser.html#xs:36"><span class="id" title="variable">xs</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">steps'</span>, <a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">t</span><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <span class="id" title="var">xs'</span><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#many_helper:37"><span class="id" title="definition">many_helper</span></a> <a class="idref" href="ImpParser.html#p:33"><span class="id" title="variable">p</span></a> (<span class="id" title="var">t</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a> <a class="idref" href="ImpParser.html#acc:34"><span class="id" title="variable">acc</span></a>) <span class="id" title="var">steps'</span> <span class="id" title="var">xs'</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
A (step-indexed) parser that expects zero or more <span class="inlinecode"><span class="id" title="var">p</span></span>s: 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="many" class="idref" href="#many"><span class="id" title="definition">many</span></a> {<a id="T:39" class="idref" href="#T:39"><span class="id" title="binder">T</span></a>} (<a id="p:40" class="idref" href="#p:40"><span class="id" title="binder">p</span></a> : <a class="idref" href="ImpParser.html#parser"><span class="id" title="definition">parser</span></a> <a class="idref" href="ImpParser.html#T:39"><span class="id" title="variable">T</span></a>) (<a id="steps:41" class="idref" href="#steps:41"><span class="id" title="binder">steps</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) : <a class="idref" href="ImpParser.html#parser"><span class="id" title="definition">parser</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="ImpParser.html#T:39"><span class="id" title="variable">T</span></a>) :=<br/>
&nbsp;&nbsp;<a class="idref" href="ImpParser.html#many_helper"><span class="id" title="definition">many_helper</span></a> <a class="idref" href="ImpParser.html#p:40"><span class="id" title="variable">p</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#ae9a5e1034e143b218b09d8e454472bd"><span class="id" title="notation">[]</span></a> <a class="idref" href="ImpParser.html#steps:41"><span class="id" title="variable">steps</span></a>.<br/>
</div>

<div class="doc">
A parser that expects a given token, followed by <span class="inlinecode"><span class="id" title="var">p</span></span>: 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="firstExpect" class="idref" href="#firstExpect"><span class="id" title="definition">firstExpect</span></a> {<a id="T:42" class="idref" href="#T:42"><span class="id" title="binder">T</span></a>} (<a id="t:43" class="idref" href="#t:43"><span class="id" title="binder">t</span></a> : <a class="idref" href="ImpParser.html#token"><span class="id" title="definition">token</span></a>) (<a id="p:44" class="idref" href="#p:44"><span class="id" title="binder">p</span></a> : <a class="idref" href="ImpParser.html#parser"><span class="id" title="definition">parser</span></a> <a class="idref" href="ImpParser.html#T:42"><span class="id" title="variable">T</span></a>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <a class="idref" href="ImpParser.html#parser"><span class="id" title="definition">parser</span></a> <a class="idref" href="ImpParser.html#T:42"><span class="id" title="variable">T</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">fun</span> <a id="xs:45" class="idref" href="#xs:45"><span class="id" title="binder">xs</span></a> ⇒ <span class="id" title="keyword">match</span> <a class="idref" href="ImpParser.html#xs:45"><span class="id" title="variable">xs</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a><span class="id" title="var">xs'</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string_dec"><span class="id" title="definition">string_dec</span></a> <span class="id" title="var">x</span> <a class="idref" href="ImpParser.html#t:43"><span class="id" title="variable">t</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">then</span> <a class="idref" href="ImpParser.html#p:44"><span class="id" title="variable">p</span></a> <span class="id" title="var">xs'</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">else</span> <a class="idref" href="ImpParser.html#NoneE"><span class="id" title="constructor">NoneE</span></a> ("expected '" <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#169ad156fbc6036a53a0338819a2b301"><span class="id" title="notation">++</span></a> <a class="idref" href="ImpParser.html#t:43"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#169ad156fbc6036a53a0338819a2b301"><span class="id" title="notation">++</span></a> "'.")<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#ae9a5e1034e143b218b09d8e454472bd"><span class="id" title="notation">[]</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#NoneE"><span class="id" title="constructor">NoneE</span></a> ("expected '" <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#169ad156fbc6036a53a0338819a2b301"><span class="id" title="notation">++</span></a> <a class="idref" href="ImpParser.html#t:43"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#169ad156fbc6036a53a0338819a2b301"><span class="id" title="notation">++</span></a> "'.")<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
A parser that expects a particular token: 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="expect" class="idref" href="#expect"><span class="id" title="definition">expect</span></a> (<a id="t:47" class="idref" href="#t:47"><span class="id" title="binder">t</span></a> : <a class="idref" href="ImpParser.html#token"><span class="id" title="definition">token</span></a>) : <a class="idref" href="ImpParser.html#parser"><span class="id" title="definition">parser</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> :=<br/>
&nbsp;&nbsp;<a class="idref" href="ImpParser.html#firstExpect"><span class="id" title="definition">firstExpect</span></a> <a class="idref" href="ImpParser.html#t:47"><span class="id" title="variable">t</span></a> (<span class="id" title="keyword">fun</span> <a id="xs:48" class="idref" href="#xs:48"><span class="id" title="binder">xs</span></a> ⇒ <a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#tt"><span class="id" title="constructor">tt</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ImpParser.html#xs:48"><span class="id" title="variable">xs</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a>).<br/>
</div>

<div class="doc">
<a id="lab389"></a><h3 class="section">A Recursive-Descent Parser for Imp</h3>

<div class="paragraph"> </div>

 Identifiers: 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="parseIdentifier" class="idref" href="#parseIdentifier"><span class="id" title="definition">parseIdentifier</span></a> (<a id="xs:49" class="idref" href="#xs:49"><span class="id" title="binder">xs</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="ImpParser.html#token"><span class="id" title="definition">token</span></a>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <a class="idref" href="ImpParser.html#optionE"><span class="id" title="inductive">optionE</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="ImpParser.html#token"><span class="id" title="definition">token</span></a>) :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="ImpParser.html#xs:49"><span class="id" title="variable">xs</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#ae9a5e1034e143b218b09d8e454472bd"><span class="id" title="notation">[]</span></a> ⇒ <a class="idref" href="ImpParser.html#NoneE"><span class="id" title="constructor">NoneE</span></a> "Expected identifier"<br/>
| <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a><span class="id" title="var">xs'</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#forallb"><span class="id" title="definition">forallb</span></a> <a class="idref" href="ImpParser.html#isLowerAlpha"><span class="id" title="definition">isLowerAlpha</span></a> (<a class="idref" href="ImpParser.html#list_of_string"><span class="id" title="definition">list_of_string</span></a> <span class="id" title="var">x</span>) <span class="id" title="keyword">then</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <span class="id" title="var">xs'</span><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">else</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#NoneE"><span class="id" title="constructor">NoneE</span></a> ("Illegal identifier:'" <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#169ad156fbc6036a53a0338819a2b301"><span class="id" title="notation">++</span></a> <span class="id" title="var">x</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#169ad156fbc6036a53a0338819a2b301"><span class="id" title="notation">++</span></a> "'")<br/>
<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
Numbers: 
</div>
<div class="code">

<span class="id" title="keyword">Definition</span> <a id="parseNumber" class="idref" href="#parseNumber"><span class="id" title="definition">parseNumber</span></a> (<a id="xs:51" class="idref" href="#xs:51"><span class="id" title="binder">xs</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="ImpParser.html#token"><span class="id" title="definition">token</span></a>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <a class="idref" href="ImpParser.html#optionE"><span class="id" title="inductive">optionE</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="ImpParser.html#token"><span class="id" title="definition">token</span></a>) :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="ImpParser.html#xs:51"><span class="id" title="variable">xs</span></a> <span class="id" title="keyword">with</span><br/>
| <a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#ae9a5e1034e143b218b09d8e454472bd"><span class="id" title="notation">[]</span></a> ⇒ <a class="idref" href="ImpParser.html#NoneE"><span class="id" title="constructor">NoneE</span></a> "Expected number"<br/>
| <span class="id" title="var">x</span><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a><span class="id" title="var">xs'</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#forallb"><span class="id" title="definition">forallb</span></a> <a class="idref" href="ImpParser.html#isDigit"><span class="id" title="definition">isDigit</span></a> (<a class="idref" href="ImpParser.html#list_of_string"><span class="id" title="definition">list_of_string</span></a> <span class="id" title="var">x</span>) <span class="id" title="keyword">then</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#fold_left"><span class="id" title="definition">fold_left</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" title="keyword">fun</span> <a id="n:53" class="idref" href="#n:53"><span class="id" title="binder">n</span></a> <a id="d:54" class="idref" href="#d:54"><span class="id" title="binder">d</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;10 <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Nat.html#ea2ff3d561159081cea6fb2e8113cc<sub>54</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="ImpParser.html#n:53"><span class="id" title="variable">n</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Nat.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">+</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Nat.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Strings.Ascii.html#nat_of_ascii"><span class="id" title="definition">nat_of_ascii</span></a> <a class="idref" href="ImpParser.html#d:54"><span class="id" title="variable">d</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Nat.html#::nat_scope:x_'-'_x"><span class="id" title="notation">-</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Strings.Ascii.html#nat_of_ascii"><span class="id" title="definition">nat_of_ascii</span></a> "0"%<span class="id" title="var">char</span><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Nat.html#0dacc1786c5ba797d47dd85006231633"><span class="id" title="notation">)</span></a>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="ImpParser.html#list_of_string"><span class="id" title="definition">list_of_string</span></a> <span class="id" title="var">x</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;0<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">xs'</span><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">else</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#NoneE"><span class="id" title="constructor">NoneE</span></a> "Expected number"<br/>
<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
Parse arithmetic expressions 
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="parsePrimaryExp" class="idref" href="#parsePrimaryExp"><span class="id" title="definition">parsePrimaryExp</span></a> (<a id="steps:55" class="idref" href="#steps:55"><span class="id" title="binder">steps</span></a>:<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a id="xs:56" class="idref" href="#xs:56"><span class="id" title="binder">xs</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="ImpParser.html#token"><span class="id" title="definition">token</span></a>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <a class="idref" href="ImpParser.html#optionE"><span class="id" title="inductive">optionE</span></a> (<a class="idref" href="Imp.html#aexp"><span class="id" title="inductive">aexp</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="ImpParser.html#token"><span class="id" title="definition">token</span></a>) :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="ImpParser.html#steps:55"><span class="id" title="variable">steps</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| 0 ⇒ <a class="idref" href="ImpParser.html#NoneE"><span class="id" title="constructor">NoneE</span></a> "Too many recursive calls"<br/>
&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">steps'</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">TRY</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">'</span></a> <a id="pat:67" class="idref" href="#pat:67"><span class="id" title="binder">(</span></a><a id="pat:67" class="idref" href="#pat:67"><span class="id" title="binder">i</span></a><a id="pat:67" class="idref" href="#pat:67"><span class="id" title="binder">,</span></a> <a id="pat:67" class="idref" href="#pat:67"><span class="id" title="binder">rest</span></a><a id="pat:67" class="idref" href="#pat:67"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="ImpParser.html#parseIdentifier"><span class="id" title="definition">parseIdentifier</span></a> <a class="idref" href="ImpParser.html#xs:56"><span class="id" title="variable">xs</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Imp.html#AId"><span class="id" title="constructor">AId</span></a> <a class="idref" href="ImpParser.html#i:66"><span class="id" title="variable">i</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ImpParser.html#rest:65"><span class="id" title="variable">rest</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">OR</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">TRY</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">'</span></a> <a id="pat:70" class="idref" href="#pat:70"><span class="id" title="binder">(</span></a><a id="pat:70" class="idref" href="#pat:70"><span class="id" title="binder">n</span></a><a id="pat:70" class="idref" href="#pat:70"><span class="id" title="binder">,</span></a> <a id="pat:70" class="idref" href="#pat:70"><span class="id" title="binder">rest</span></a><a id="pat:70" class="idref" href="#pat:70"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="ImpParser.html#parseNumber"><span class="id" title="definition">parseNumber</span></a> <a class="idref" href="ImpParser.html#xs:56"><span class="id" title="variable">xs</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Imp.html#ANum"><span class="id" title="constructor">ANum</span></a> <a class="idref" href="ImpParser.html#n:69"><span class="id" title="variable">n</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ImpParser.html#rest:68"><span class="id" title="variable">rest</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">OR</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">'</span></a> <a id="pat:73" class="idref" href="#pat:73"><span class="id" title="binder">(</span></a><a id="pat:73" class="idref" href="#pat:73"><span class="id" title="binder">e</span></a><a id="pat:73" class="idref" href="#pat:73"><span class="id" title="binder">,</span></a> <a id="pat:73" class="idref" href="#pat:73"><span class="id" title="binder">rest</span></a><a id="pat:73" class="idref" href="#pat:73"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="ImpParser.html#firstExpect"><span class="id" title="definition">firstExpect</span></a> "(" (<a class="idref" href="ImpParser.html#parseSumExp:63"><span class="id" title="definition">parseSumExp</span></a> <span class="id" title="var">steps'</span>) <a class="idref" href="ImpParser.html#xs:56"><span class="id" title="variable">xs</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">'</span></a> <a id="pat:76" class="idref" href="#pat:76"><span class="id" title="binder">(</span></a><a id="pat:76" class="idref" href="#pat:76"><span class="id" title="binder">u</span></a><a id="pat:76" class="idref" href="#pat:76"><span class="id" title="binder">,</span></a> <a id="pat:76" class="idref" href="#pat:76"><span class="id" title="binder">rest'</span></a><a id="pat:76" class="idref" href="#pat:76"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="ImpParser.html#expect"><span class="id" title="definition">expect</span></a> ")" <a class="idref" href="ImpParser.html#rest:71"><span class="id" title="variable">rest</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="ImpParser.html#e:72"><span class="id" title="variable">e</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a><a class="idref" href="ImpParser.html#rest':74"><span class="id" title="variable">rest'</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
<br/>
<span class="id" title="keyword">with</span> <a id="parseProductExp" class="idref" href="#parseProductExp"><span class="id" title="definition">parseProductExp</span></a> (<a id="steps:57" class="idref" href="#steps:57"><span class="id" title="binder">steps</span></a>:<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a id="xs:58" class="idref" href="#xs:58"><span class="id" title="binder">xs</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="ImpParser.html#token"><span class="id" title="definition">token</span></a>) :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="ImpParser.html#steps:57"><span class="id" title="variable">steps</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| 0 ⇒ <a class="idref" href="ImpParser.html#NoneE"><span class="id" title="constructor">NoneE</span></a> "Too many recursive calls"<br/>
&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">steps'</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">'</span></a> <a id="pat:80" class="idref" href="#pat:80"><span class="id" title="binder">(</span></a><a id="pat:80" class="idref" href="#pat:80"><span class="id" title="binder">e</span></a><a id="pat:80" class="idref" href="#pat:80"><span class="id" title="binder">,</span></a> <a id="pat:80" class="idref" href="#pat:80"><span class="id" title="binder">rest</span></a><a id="pat:80" class="idref" href="#pat:80"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="ImpParser.html#parsePrimaryExp:61"><span class="id" title="definition">parsePrimaryExp</span></a> <span class="id" title="var">steps'</span> <a class="idref" href="ImpParser.html#xs:58"><span class="id" title="variable">xs</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">'</span></a> <a id="pat:83" class="idref" href="#pat:83"><span class="id" title="binder">(</span></a><a id="pat:83" class="idref" href="#pat:83"><span class="id" title="binder">es</span></a><a id="pat:83" class="idref" href="#pat:83"><span class="id" title="binder">,</span></a> <a id="pat:83" class="idref" href="#pat:83"><span class="id" title="binder">rest'</span></a><a id="pat:83" class="idref" href="#pat:83"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="ImpParser.html#many"><span class="id" title="definition">many</span></a> (<a class="idref" href="ImpParser.html#firstExpect"><span class="id" title="definition">firstExpect</span></a> "*" (<a class="idref" href="ImpParser.html#parsePrimaryExp:61"><span class="id" title="definition">parsePrimaryExp</span></a> <span class="id" title="var">steps'</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">steps'</span> <a class="idref" href="ImpParser.html#rest:78"><span class="id" title="variable">rest</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#fold_left"><span class="id" title="definition">fold_left</span></a> <a class="idref" href="Imp.html#AMult"><span class="id" title="constructor">AMult</span></a> <a class="idref" href="ImpParser.html#es:82"><span class="id" title="variable">es</span></a> <a class="idref" href="ImpParser.html#e:79"><span class="id" title="variable">e</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ImpParser.html#rest':81"><span class="id" title="variable">rest'</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
<br/>
<span class="id" title="keyword">with</span> <a id="parseSumExp" class="idref" href="#parseSumExp"><span class="id" title="definition">parseSumExp</span></a> (<a id="steps:59" class="idref" href="#steps:59"><span class="id" title="binder">steps</span></a>:<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>) (<a id="xs:60" class="idref" href="#xs:60"><span class="id" title="binder">xs</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="ImpParser.html#token"><span class="id" title="definition">token</span></a>)  :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="ImpParser.html#steps:59"><span class="id" title="variable">steps</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| 0 ⇒ <a class="idref" href="ImpParser.html#NoneE"><span class="id" title="constructor">NoneE</span></a> "Too many recursive calls"<br/>
&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">steps'</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">'</span></a> <a id="pat:87" class="idref" href="#pat:87"><span class="id" title="binder">(</span></a><a id="pat:87" class="idref" href="#pat:87"><span class="id" title="binder">e</span></a><a id="pat:87" class="idref" href="#pat:87"><span class="id" title="binder">,</span></a> <a id="pat:87" class="idref" href="#pat:87"><span class="id" title="binder">rest</span></a><a id="pat:87" class="idref" href="#pat:87"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="ImpParser.html#parseProductExp:62"><span class="id" title="definition">parseProductExp</span></a> <span class="id" title="var">steps'</span> <a class="idref" href="ImpParser.html#xs:60"><span class="id" title="variable">xs</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">'</span></a> <a id="pat:97" class="idref" href="#pat:97"><span class="id" title="binder">(</span></a><a id="pat:97" class="idref" href="#pat:97"><span class="id" title="binder">es</span></a><a id="pat:97" class="idref" href="#pat:97"><span class="id" title="binder">,</span></a> <a id="pat:97" class="idref" href="#pat:97"><span class="id" title="binder">rest'</span></a><a id="pat:97" class="idref" href="#pat:97"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">&lt;-</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#many"><span class="id" title="definition">many</span></a> (<span class="id" title="keyword">fun</span> <a id="xs:88" class="idref" href="#xs:88"><span class="id" title="binder">xs</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">TRY</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">'</span></a> <a id="pat:91" class="idref" href="#pat:91"><span class="id" title="binder">(</span></a><a id="pat:91" class="idref" href="#pat:91"><span class="id" title="binder">e</span></a><a id="pat:91" class="idref" href="#pat:91"><span class="id" title="binder">,</span></a><a id="pat:91" class="idref" href="#pat:91"><span class="id" title="binder">rest'</span></a><a id="pat:91" class="idref" href="#pat:91"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">&lt;-</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#firstExpect"><span class="id" title="definition">firstExpect</span></a> "+"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="ImpParser.html#parseProductExp:62"><span class="id" title="definition">parseProductExp</span></a> <span class="id" title="var">steps'</span>) <a class="idref" href="ImpParser.html#xs:88"><span class="id" title="variable">xs</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Imp.html#:::'true'"><span class="id" title="notation">true</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ImpParser.html#e:90"><span class="id" title="variable">e</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">),</span></a> <a class="idref" href="ImpParser.html#rest':89"><span class="id" title="variable">rest'</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">OR</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">'</span></a> <a id="pat:94" class="idref" href="#pat:94"><span class="id" title="binder">(</span></a><a id="pat:94" class="idref" href="#pat:94"><span class="id" title="binder">e</span></a><a id="pat:94" class="idref" href="#pat:94"><span class="id" title="binder">,</span></a> <a id="pat:94" class="idref" href="#pat:94"><span class="id" title="binder">rest'</span></a><a id="pat:94" class="idref" href="#pat:94"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">&lt;-</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#firstExpect"><span class="id" title="definition">firstExpect</span></a> "-"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="ImpParser.html#parseProductExp:62"><span class="id" title="definition">parseProductExp</span></a> <span class="id" title="var">steps'</span>) <a class="idref" href="ImpParser.html#xs:88"><span class="id" title="variable">xs</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Imp.html#:::'false'"><span class="id" title="notation">false</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ImpParser.html#e:93"><span class="id" title="variable">e</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">),</span></a> <a class="idref" href="ImpParser.html#rest':92"><span class="id" title="variable">rest'</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">steps'</span> <a class="idref" href="ImpParser.html#rest:85"><span class="id" title="variable">rest</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#fold_left"><span class="id" title="definition">fold_left</span></a> (<span class="id" title="keyword">fun</span> <a id="e<sub>0</sub>:98" class="idref" href="#e<sub>0</sub>:98"><span class="id" title="binder">e<sub>0</sub></span></a> <a id="term:99" class="idref" href="#term:99"><span class="id" title="binder">term</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="ImpParser.html#term:99"><span class="id" title="variable">term</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Imp.html#:::'true'"><span class="id" title="notation">true</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a>  <span class="id" title="var">e</span><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> ⇒ <a class="idref" href="Imp.html#APlus"><span class="id" title="constructor">APlus</span></a> <a class="idref" href="ImpParser.html#e<sub>0</sub>:98"><span class="id" title="variable">e<sub>0</sub></span></a> <a class="idref" href="ImpParser.html#e:86"><span class="id" title="variable">e</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Imp.html#:::'false'"><span class="id" title="notation">false</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <span class="id" title="var">e</span><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> ⇒ <a class="idref" href="Imp.html#AMinus"><span class="id" title="constructor">AMinus</span></a> <a class="idref" href="ImpParser.html#e<sub>0</sub>:98"><span class="id" title="variable">e<sub>0</sub></span></a> <a class="idref" href="ImpParser.html#e:86"><span class="id" title="variable">e</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#es:96"><span class="id" title="variable">es</span></a> <a class="idref" href="ImpParser.html#e:86"><span class="id" title="variable">e</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#rest':95"><span class="id" title="variable">rest'</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="parseAExp" class="idref" href="#parseAExp"><span class="id" title="definition">parseAExp</span></a> := <a class="idref" href="ImpParser.html#parseSumExp"><span class="id" title="definition">parseSumExp</span></a>.<br/>
</div>

<div class="doc">
Parsing boolean expressions: 
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="parseAtomicExp" class="idref" href="#parseAtomicExp"><span class="id" title="definition">parseAtomicExp</span></a> (<a id="steps:101" class="idref" href="#steps:101"><span class="id" title="binder">steps</span></a>:<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a id="xs:102" class="idref" href="#xs:102"><span class="id" title="binder">xs</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="ImpParser.html#token"><span class="id" title="definition">token</span></a>)  :=<br/>
<span class="id" title="keyword">match</span> <a class="idref" href="ImpParser.html#steps:101"><span class="id" title="variable">steps</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| 0 ⇒ <a class="idref" href="ImpParser.html#NoneE"><span class="id" title="constructor">NoneE</span></a> "Too many recursive calls"<br/>
&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">steps'</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">TRY</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">'</span></a> <a id="pat:110" class="idref" href="#pat:110"><span class="id" title="binder">(</span></a><a id="pat:110" class="idref" href="#pat:110"><span class="id" title="binder">u</span></a><a id="pat:110" class="idref" href="#pat:110"><span class="id" title="binder">,</span></a><a id="pat:110" class="idref" href="#pat:110"><span class="id" title="binder">rest</span></a><a id="pat:110" class="idref" href="#pat:110"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="ImpParser.html#expect"><span class="id" title="definition">expect</span></a> "true" <a class="idref" href="ImpParser.html#xs:102"><span class="id" title="variable">xs</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Imp.html#BTrue"><span class="id" title="constructor">BTrue</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a><a class="idref" href="ImpParser.html#rest:108"><span class="id" title="variable">rest</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">OR</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">TRY</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">'</span></a> <a id="pat:113" class="idref" href="#pat:113"><span class="id" title="binder">(</span></a><a id="pat:113" class="idref" href="#pat:113"><span class="id" title="binder">u</span></a><a id="pat:113" class="idref" href="#pat:113"><span class="id" title="binder">,</span></a><a id="pat:113" class="idref" href="#pat:113"><span class="id" title="binder">rest</span></a><a id="pat:113" class="idref" href="#pat:113"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="ImpParser.html#expect"><span class="id" title="definition">expect</span></a> "false" <a class="idref" href="ImpParser.html#xs:102"><span class="id" title="variable">xs</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Imp.html#BFalse"><span class="id" title="constructor">BFalse</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a><a class="idref" href="ImpParser.html#rest:111"><span class="id" title="variable">rest</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">OR</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">TRY</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">'</span></a> <a id="pat:116" class="idref" href="#pat:116"><span class="id" title="binder">(</span></a><a id="pat:116" class="idref" href="#pat:116"><span class="id" title="binder">e</span></a><a id="pat:116" class="idref" href="#pat:116"><span class="id" title="binder">,</span></a><a id="pat:116" class="idref" href="#pat:116"><span class="id" title="binder">rest</span></a><a id="pat:116" class="idref" href="#pat:116"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="ImpParser.html#firstExpect"><span class="id" title="definition">firstExpect</span></a> "~"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="ImpParser.html#parseAtomicExp:105"><span class="id" title="definition">parseAtomicExp</span></a> <span class="id" title="var">steps'</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#xs:102"><span class="id" title="variable">xs</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Imp.html#BNot"><span class="id" title="constructor">BNot</span></a> <a class="idref" href="ImpParser.html#e:115"><span class="id" title="variable">e</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ImpParser.html#rest:114"><span class="id" title="variable">rest</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">OR</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">TRY</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">'</span></a> <a id="pat:119" class="idref" href="#pat:119"><span class="id" title="binder">(</span></a><a id="pat:119" class="idref" href="#pat:119"><span class="id" title="binder">e</span></a><a id="pat:119" class="idref" href="#pat:119"><span class="id" title="binder">,</span></a><a id="pat:119" class="idref" href="#pat:119"><span class="id" title="binder">rest</span></a><a id="pat:119" class="idref" href="#pat:119"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="ImpParser.html#firstExpect"><span class="id" title="definition">firstExpect</span></a> "("<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="ImpParser.html#parseConjunctionExp:106"><span class="id" title="definition">parseConjunctionExp</span></a> <span class="id" title="var">steps'</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#xs:102"><span class="id" title="variable">xs</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">'</span></a> <a id="pat:122" class="idref" href="#pat:122"><span class="id" title="binder">(</span></a><a id="pat:122" class="idref" href="#pat:122"><span class="id" title="binder">u</span></a><a id="pat:122" class="idref" href="#pat:122"><span class="id" title="binder">,</span></a><a id="pat:122" class="idref" href="#pat:122"><span class="id" title="binder">rest'</span></a><a id="pat:122" class="idref" href="#pat:122"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="ImpParser.html#expect"><span class="id" title="definition">expect</span></a> ")" <a class="idref" href="ImpParser.html#rest:117"><span class="id" title="variable">rest</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="ImpParser.html#e:118"><span class="id" title="variable">e</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ImpParser.html#rest':120"><span class="id" title="variable">rest'</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">OR</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">'</span></a> <a id="pat:125" class="idref" href="#pat:125"><span class="id" title="binder">(</span></a><a id="pat:125" class="idref" href="#pat:125"><span class="id" title="binder">e</span></a><a id="pat:125" class="idref" href="#pat:125"><span class="id" title="binder">,</span></a> <a id="pat:125" class="idref" href="#pat:125"><span class="id" title="binder">rest</span></a><a id="pat:125" class="idref" href="#pat:125"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="ImpParser.html#parseProductExp"><span class="id" title="definition">parseProductExp</span></a> <span class="id" title="var">steps'</span> <a class="idref" href="ImpParser.html#xs:102"><span class="id" title="variable">xs</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">TRY</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">'</span></a> <a id="pat:128" class="idref" href="#pat:128"><span class="id" title="binder">(</span></a><a id="pat:128" class="idref" href="#pat:128"><span class="id" title="binder">e'</span></a><a id="pat:128" class="idref" href="#pat:128"><span class="id" title="binder">,</span></a> <a id="pat:128" class="idref" href="#pat:128"><span class="id" title="binder">rest'</span></a><a id="pat:128" class="idref" href="#pat:128"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="ImpParser.html#firstExpect"><span class="id" title="definition">firstExpect</span></a> "="<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="ImpParser.html#parseAExp"><span class="id" title="definition">parseAExp</span></a> <span class="id" title="var">steps'</span>) <a class="idref" href="ImpParser.html#rest:123"><span class="id" title="variable">rest</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Imp.html#BEq"><span class="id" title="constructor">BEq</span></a> <a class="idref" href="ImpParser.html#e:124"><span class="id" title="variable">e</span></a> <a class="idref" href="ImpParser.html#e':127"><span class="id" title="variable">e'</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ImpParser.html#rest':126"><span class="id" title="variable">rest'</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">OR</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">TRY</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">'</span></a> <a id="pat:131" class="idref" href="#pat:131"><span class="id" title="binder">(</span></a><a id="pat:131" class="idref" href="#pat:131"><span class="id" title="binder">e'</span></a><a id="pat:131" class="idref" href="#pat:131"><span class="id" title="binder">,</span></a> <a id="pat:131" class="idref" href="#pat:131"><span class="id" title="binder">rest'</span></a><a id="pat:131" class="idref" href="#pat:131"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="ImpParser.html#firstExpect"><span class="id" title="definition">firstExpect</span></a> "&lt;="<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="ImpParser.html#parseAExp"><span class="id" title="definition">parseAExp</span></a> <span class="id" title="var">steps'</span>) <a class="idref" href="ImpParser.html#rest:123"><span class="id" title="variable">rest</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Imp.html#BLe"><span class="id" title="constructor">BLe</span></a> <a class="idref" href="ImpParser.html#e:124"><span class="id" title="variable">e</span></a> <a class="idref" href="ImpParser.html#e':130"><span class="id" title="variable">e'</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ImpParser.html#rest':129"><span class="id" title="variable">rest'</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">OR</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#NoneE"><span class="id" title="constructor">NoneE</span></a> "Expected '=' or '&lt;=' after arithmetic expression"<br/>
<span class="id" title="keyword">end</span><br/>
<br/>
<span class="id" title="keyword">with</span> <a id="parseConjunctionExp" class="idref" href="#parseConjunctionExp"><span class="id" title="definition">parseConjunctionExp</span></a> (<a id="steps:103" class="idref" href="#steps:103"><span class="id" title="binder">steps</span></a>:<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a id="xs:104" class="idref" href="#xs:104"><span class="id" title="binder">xs</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="ImpParser.html#token"><span class="id" title="definition">token</span></a>) :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="ImpParser.html#steps:103"><span class="id" title="variable">steps</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| 0 ⇒ <a class="idref" href="ImpParser.html#NoneE"><span class="id" title="constructor">NoneE</span></a> "Too many recursive calls"<br/>
&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">steps'</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">'</span></a> <a id="pat:135" class="idref" href="#pat:135"><span class="id" title="binder">(</span></a><a id="pat:135" class="idref" href="#pat:135"><span class="id" title="binder">e</span></a><a id="pat:135" class="idref" href="#pat:135"><span class="id" title="binder">,</span></a> <a id="pat:135" class="idref" href="#pat:135"><span class="id" title="binder">rest</span></a><a id="pat:135" class="idref" href="#pat:135"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="ImpParser.html#parseAtomicExp:105"><span class="id" title="definition">parseAtomicExp</span></a> <span class="id" title="var">steps'</span> <a class="idref" href="ImpParser.html#xs:104"><span class="id" title="variable">xs</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">'</span></a> <a id="pat:138" class="idref" href="#pat:138"><span class="id" title="binder">(</span></a><a id="pat:138" class="idref" href="#pat:138"><span class="id" title="binder">es</span></a><a id="pat:138" class="idref" href="#pat:138"><span class="id" title="binder">,</span></a> <a id="pat:138" class="idref" href="#pat:138"><span class="id" title="binder">rest'</span></a><a id="pat:138" class="idref" href="#pat:138"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="ImpParser.html#many"><span class="id" title="definition">many</span></a> (<a class="idref" href="ImpParser.html#firstExpect"><span class="id" title="definition">firstExpect</span></a> "&amp;&amp;"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="ImpParser.html#parseAtomicExp:105"><span class="id" title="definition">parseAtomicExp</span></a> <span class="id" title="var">steps'</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">steps'</span> <a class="idref" href="ImpParser.html#rest:133"><span class="id" title="variable">rest</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#fold_left"><span class="id" title="definition">fold_left</span></a> <a class="idref" href="Imp.html#BAnd"><span class="id" title="constructor">BAnd</span></a> <a class="idref" href="ImpParser.html#es:137"><span class="id" title="variable">es</span></a> <a class="idref" href="ImpParser.html#e:134"><span class="id" title="variable">e</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ImpParser.html#rest':136"><span class="id" title="variable">rest'</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="parseBExp" class="idref" href="#parseBExp"><span class="id" title="definition">parseBExp</span></a> := <a class="idref" href="ImpParser.html#parseConjunctionExp"><span class="id" title="definition">parseConjunctionExp</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Check</span> <a class="idref" href="ImpParser.html#parseConjunctionExp"><span class="id" title="definition">parseConjunctionExp</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="testParsing" class="idref" href="#testParsing"><span class="id" title="definition">testParsing</span></a> {<a id="X:139" class="idref" href="#X:139"><span class="id" title="binder">X</span></a> : <span class="id" title="keyword">Type</span>}<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a id="p:140" class="idref" href="#p:140"><span class="id" title="binder">p</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="ImpParser.html#token"><span class="id" title="definition">token</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#optionE"><span class="id" title="inductive">optionE</span></a> (<a class="idref" href="ImpParser.html#X:139"><span class="id" title="variable">X</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="ImpParser.html#token"><span class="id" title="definition">token</span></a>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a id="s:141" class="idref" href="#s:141"><span class="id" title="binder">s</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">let</span> <a id="t:142" class="idref" href="#t:142"><span class="id" title="binder">t</span></a> := <a class="idref" href="ImpParser.html#tokenize"><span class="id" title="definition">tokenize</span></a> <a class="idref" href="ImpParser.html#s:141"><span class="id" title="variable">s</span></a> <span class="id" title="keyword">in</span><br/>
&nbsp;&nbsp;<a class="idref" href="ImpParser.html#p:140"><span class="id" title="variable">p</span></a> 100 <a class="idref" href="ImpParser.html#t:142"><span class="id" title="variable">t</span></a>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*<br/>
Eval&nbsp;compute&nbsp;in<br/>
&nbsp;&nbsp;testParsing&nbsp;parseProductExp&nbsp;"x.y.(x.x).x".<br/>
<br/>
Eval&nbsp;compute&nbsp;in<br/>
&nbsp;&nbsp;testParsing&nbsp;parseConjunctionExp&nbsp;"~(x=x&amp;&amp;x*x&lt;=(x*x)*x)&amp;&amp;x=x".<br/>
*)</span><br/>
</div>

<div class="doc">
Parsing commands: 
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="parseSimpleCommand" class="idref" href="#parseSimpleCommand"><span class="id" title="definition">parseSimpleCommand</span></a> (<a id="steps:143" class="idref" href="#steps:143"><span class="id" title="binder">steps</span></a>:<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a id="xs:144" class="idref" href="#xs:144"><span class="id" title="binder">xs</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="ImpParser.html#token"><span class="id" title="definition">token</span></a>) :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="ImpParser.html#steps:143"><span class="id" title="variable">steps</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| 0 ⇒ <a class="idref" href="ImpParser.html#NoneE"><span class="id" title="constructor">NoneE</span></a> "Too many recursive calls"<br/>
&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">steps'</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">TRY</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">'</span></a> <a id="pat:152" class="idref" href="#pat:152"><span class="id" title="binder">(</span></a><a id="pat:152" class="idref" href="#pat:152"><span class="id" title="binder">u</span></a><a id="pat:152" class="idref" href="#pat:152"><span class="id" title="binder">,</span></a> <a id="pat:152" class="idref" href="#pat:152"><span class="id" title="binder">rest</span></a><a id="pat:152" class="idref" href="#pat:152"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="ImpParser.html#expect"><span class="id" title="definition">expect</span></a> "skip" <a class="idref" href="ImpParser.html#xs:144"><span class="id" title="variable">xs</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Imp.html#23430cd9e427d30c054d4f029e39cb7f"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Imp.html#:com:com_scope:'skip'"><span class="id" title="notation">skip</span></a><a class="idref" href="Imp.html#23430cd9e427d30c054d4f029e39cb7f"><span class="id" title="notation">}&gt;</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ImpParser.html#rest:150"><span class="id" title="variable">rest</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">OR</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">TRY</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">'</span></a> <a id="pat:155" class="idref" href="#pat:155"><span class="id" title="binder">(</span></a><a id="pat:155" class="idref" href="#pat:155"><span class="id" title="binder">e</span></a><a id="pat:155" class="idref" href="#pat:155"><span class="id" title="binder">,</span></a><a id="pat:155" class="idref" href="#pat:155"><span class="id" title="binder">rest</span></a><a id="pat:155" class="idref" href="#pat:155"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">&lt;-</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#firstExpect"><span class="id" title="definition">firstExpect</span></a> "if"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="ImpParser.html#parseBExp"><span class="id" title="definition">parseBExp</span></a> <span class="id" title="var">steps'</span>) <a class="idref" href="ImpParser.html#xs:144"><span class="id" title="variable">xs</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">'</span></a> <a id="pat:158" class="idref" href="#pat:158"><span class="id" title="binder">(</span></a><a id="pat:158" class="idref" href="#pat:158"><span class="id" title="binder">c</span></a><a id="pat:158" class="idref" href="#pat:158"><span class="id" title="binder">,</span></a><a id="pat:158" class="idref" href="#pat:158"><span class="id" title="binder">rest'</span></a><a id="pat:158" class="idref" href="#pat:158"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">&lt;-</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#firstExpect"><span class="id" title="definition">firstExpect</span></a> "then"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="ImpParser.html#parseSequencedCommand:148"><span class="id" title="definition">parseSequencedCommand</span></a> <span class="id" title="var">steps'</span>) <a class="idref" href="ImpParser.html#rest:153"><span class="id" title="variable">rest</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">'</span></a> <a id="pat:161" class="idref" href="#pat:161"><span class="id" title="binder">(</span></a><a id="pat:161" class="idref" href="#pat:161"><span class="id" title="binder">c'</span></a><a id="pat:161" class="idref" href="#pat:161"><span class="id" title="binder">,</span></a><a id="pat:161" class="idref" href="#pat:161"><span class="id" title="binder">rest''</span></a><a id="pat:161" class="idref" href="#pat:161"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">&lt;-</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#firstExpect"><span class="id" title="definition">firstExpect</span></a> "else"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="ImpParser.html#parseSequencedCommand:148"><span class="id" title="definition">parseSequencedCommand</span></a> <span class="id" title="var">steps'</span>) <a class="idref" href="ImpParser.html#rest':156"><span class="id" title="variable">rest'</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">'</span></a> <a id="pat:163" class="idref" href="#pat:163"><span class="id" title="binder">(</span></a><a id="pat:163" class="idref" href="#pat:163"><span class="id" title="binder">tt</span></a><a id="pat:163" class="idref" href="#pat:163"><span class="id" title="binder">,</span></a><a id="pat:163" class="idref" href="#pat:163"><span class="id" title="binder">rest'''</span></a><a id="pat:163" class="idref" href="#pat:163"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">&lt;-</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#expect"><span class="id" title="definition">expect</span></a> "end" <a class="idref" href="ImpParser.html#rest'':159"><span class="id" title="variable">rest''</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Imp.html#23430cd9e427d30c054d4f029e39cb7f"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Imp.html#:com:com_scope:'if'_x_'then'_x_'else'_x_'end'"><span class="id" title="notation">if</span></a> <a class="idref" href="ImpParser.html#e:154"><span class="id" title="variable">e</span></a> <a class="idref" href="Imp.html#:com:com_scope:'if'_x_'then'_x_'else'_x_'end'"><span class="id" title="notation">then</span></a> <a class="idref" href="ImpParser.html#c:157"><span class="id" title="variable">c</span></a> <a class="idref" href="Imp.html#:com:com_scope:'if'_x_'then'_x_'else'_x_'end'"><span class="id" title="notation">else</span></a> <a class="idref" href="ImpParser.html#c':160"><span class="id" title="variable">c'</span></a> <a class="idref" href="Imp.html#:com:com_scope:'if'_x_'then'_x_'else'_x_'end'"><span class="id" title="notation">end</span></a><a class="idref" href="Imp.html#23430cd9e427d30c054d4f029e39cb7f"><span class="id" title="notation">}&gt;</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ImpParser.html#rest''':162"><span class="id" title="variable">rest'''</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">OR</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">TRY</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">'</span></a> <a id="pat:166" class="idref" href="#pat:166"><span class="id" title="binder">(</span></a><a id="pat:166" class="idref" href="#pat:166"><span class="id" title="binder">e</span></a><a id="pat:166" class="idref" href="#pat:166"><span class="id" title="binder">,</span></a><a id="pat:166" class="idref" href="#pat:166"><span class="id" title="binder">rest</span></a><a id="pat:166" class="idref" href="#pat:166"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">&lt;-</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#firstExpect"><span class="id" title="definition">firstExpect</span></a> "while"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="ImpParser.html#parseBExp"><span class="id" title="definition">parseBExp</span></a> <span class="id" title="var">steps'</span>) <a class="idref" href="ImpParser.html#xs:144"><span class="id" title="variable">xs</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">'</span></a> <a id="pat:169" class="idref" href="#pat:169"><span class="id" title="binder">(</span></a><a id="pat:169" class="idref" href="#pat:169"><span class="id" title="binder">c</span></a><a id="pat:169" class="idref" href="#pat:169"><span class="id" title="binder">,</span></a><a id="pat:169" class="idref" href="#pat:169"><span class="id" title="binder">rest'</span></a><a id="pat:169" class="idref" href="#pat:169"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">&lt;-</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#firstExpect"><span class="id" title="definition">firstExpect</span></a> "do"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="ImpParser.html#parseSequencedCommand:148"><span class="id" title="definition">parseSequencedCommand</span></a> <span class="id" title="var">steps'</span>) <a class="idref" href="ImpParser.html#rest:164"><span class="id" title="variable">rest</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">'</span></a> <a id="pat:172" class="idref" href="#pat:172"><span class="id" title="binder">(</span></a><a id="pat:172" class="idref" href="#pat:172"><span class="id" title="binder">u</span></a><a id="pat:172" class="idref" href="#pat:172"><span class="id" title="binder">,</span></a><a id="pat:172" class="idref" href="#pat:172"><span class="id" title="binder">rest''</span></a><a id="pat:172" class="idref" href="#pat:172"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">&lt;-</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#expect"><span class="id" title="definition">expect</span></a> "end" <a class="idref" href="ImpParser.html#rest':167"><span class="id" title="variable">rest'</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Imp.html#23430cd9e427d30c054d4f029e39cb7f"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Imp.html#:com:com_scope:'while'_x_'do'_x_'end'"><span class="id" title="notation">while</span></a> <a class="idref" href="ImpParser.html#e:165"><span class="id" title="variable">e</span></a> <a class="idref" href="Imp.html#:com:com_scope:'while'_x_'do'_x_'end'"><span class="id" title="notation">do</span></a> <a class="idref" href="ImpParser.html#c:168"><span class="id" title="variable">c</span></a> <a class="idref" href="Imp.html#:com:com_scope:'while'_x_'do'_x_'end'"><span class="id" title="notation">end</span></a><a class="idref" href="Imp.html#23430cd9e427d30c054d4f029e39cb7f"><span class="id" title="notation">}&gt;</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ImpParser.html#rest'':170"><span class="id" title="variable">rest''</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">OR</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">TRY</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">'</span></a> <a id="pat:175" class="idref" href="#pat:175"><span class="id" title="binder">(</span></a><a id="pat:175" class="idref" href="#pat:175"><span class="id" title="binder">i</span></a><a id="pat:175" class="idref" href="#pat:175"><span class="id" title="binder">,</span></a> <a id="pat:175" class="idref" href="#pat:175"><span class="id" title="binder">rest</span></a><a id="pat:175" class="idref" href="#pat:175"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="ImpParser.html#parseIdentifier"><span class="id" title="definition">parseIdentifier</span></a> <a class="idref" href="ImpParser.html#xs:144"><span class="id" title="variable">xs</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">'</span></a> <a id="pat:178" class="idref" href="#pat:178"><span class="id" title="binder">(</span></a><a id="pat:178" class="idref" href="#pat:178"><span class="id" title="binder">e</span></a><a id="pat:178" class="idref" href="#pat:178"><span class="id" title="binder">,</span></a> <a id="pat:178" class="idref" href="#pat:178"><span class="id" title="binder">rest'</span></a><a id="pat:178" class="idref" href="#pat:178"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="ImpParser.html#firstExpect"><span class="id" title="definition">firstExpect</span></a> ":=" (<a class="idref" href="ImpParser.html#parseAExp"><span class="id" title="definition">parseAExp</span></a> <span class="id" title="var">steps'</span>) <a class="idref" href="ImpParser.html#rest:173"><span class="id" title="variable">rest</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Imp.html#23430cd9e427d30c054d4f029e39cb7f"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="ImpParser.html#i:174"><span class="id" title="variable">i</span></a> <a class="idref" href="Imp.html#91e9aa710642047a93142bdf557f1a1b"><span class="id" title="notation">:=</span></a> <a class="idref" href="ImpParser.html#e:177"><span class="id" title="variable">e</span></a><a class="idref" href="Imp.html#23430cd9e427d30c054d4f029e39cb7f"><span class="id" title="notation">}&gt;</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ImpParser.html#rest':176"><span class="id" title="variable">rest'</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">OR</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#NoneE"><span class="id" title="constructor">NoneE</span></a> "Expecting a command"<br/>
<span class="id" title="keyword">end</span><br/>
<br/>
<span class="id" title="keyword">with</span> <a id="parseSequencedCommand" class="idref" href="#parseSequencedCommand"><span class="id" title="definition">parseSequencedCommand</span></a> (<a id="steps:145" class="idref" href="#steps:145"><span class="id" title="binder">steps</span></a>:<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a id="xs:146" class="idref" href="#xs:146"><span class="id" title="binder">xs</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#list"><span class="id" title="inductive">list</span></a> <a class="idref" href="ImpParser.html#token"><span class="id" title="definition">token</span></a>) :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="ImpParser.html#steps:145"><span class="id" title="variable">steps</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| 0 ⇒ <a class="idref" href="ImpParser.html#NoneE"><span class="id" title="constructor">NoneE</span></a> "Too many recursive calls"<br/>
&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#S"><span class="id" title="constructor">S</span></a> <span class="id" title="var">steps'</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">'</span></a> <a id="pat:182" class="idref" href="#pat:182"><span class="id" title="binder">(</span></a><a id="pat:182" class="idref" href="#pat:182"><span class="id" title="binder">c</span></a><a id="pat:182" class="idref" href="#pat:182"><span class="id" title="binder">,</span></a> <a id="pat:182" class="idref" href="#pat:182"><span class="id" title="binder">rest</span></a><a id="pat:182" class="idref" href="#pat:182"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="ImpParser.html#parseSimpleCommand:147"><span class="id" title="definition">parseSimpleCommand</span></a> <span class="id" title="var">steps'</span> <a class="idref" href="ImpParser.html#xs:146"><span class="id" title="variable">xs</span></a> <a class="idref" href="ImpParser.html#c2b4d6f0daa4552d70137fd9d8530127"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">TRY</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">'</span></a> <a id="pat:185" class="idref" href="#pat:185"><span class="id" title="binder">(</span></a><a id="pat:185" class="idref" href="#pat:185"><span class="id" title="binder">c'</span></a><a id="pat:185" class="idref" href="#pat:185"><span class="id" title="binder">,</span></a> <a id="pat:185" class="idref" href="#pat:185"><span class="id" title="binder">rest'</span></a><a id="pat:185" class="idref" href="#pat:185"><span class="id" title="binder">)</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">&lt;-</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#firstExpect"><span class="id" title="definition">firstExpect</span></a> ";"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<a class="idref" href="ImpParser.html#parseSequencedCommand:148"><span class="id" title="definition">parseSequencedCommand</span></a> <span class="id" title="var">steps'</span>) <a class="idref" href="ImpParser.html#rest:180"><span class="id" title="variable">rest</span></a> <a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="Imp.html#23430cd9e427d30c054d4f029e39cb7f"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="ImpParser.html#c:181"><span class="id" title="variable">c</span></a> <a class="idref" href="Imp.html#313afe74ec81f2da17d8e7bca3b042e<sub>7</sub>"><span class="id" title="notation">;</span></a> <a class="idref" href="ImpParser.html#c':184"><span class="id" title="variable">c'</span></a><a class="idref" href="Imp.html#23430cd9e427d30c054d4f029e39cb7f"><span class="id" title="notation">}&gt;</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ImpParser.html#rest':183"><span class="id" title="variable">rest'</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#d3681d6f57c7eee49c36b58445e43f<sub>11</sub>"><span class="id" title="notation">OR</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><a class="idref" href="ImpParser.html#c:181"><span class="id" title="variable">c</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="ImpParser.html#rest:180"><span class="id" title="variable">rest</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="bignumber" class="idref" href="#bignumber"><span class="id" title="definition">bignumber</span></a> := 1000.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Definition</span> <a id="parse" class="idref" href="#parse"><span class="id" title="definition">parse</span></a> (<a id="str:186" class="idref" href="#str:186"><span class="id" title="binder">str</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) : <a class="idref" href="ImpParser.html#optionE"><span class="id" title="inductive">optionE</span></a> <a class="idref" href="Imp.html#com"><span class="id" title="inductive">com</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">let</span> <a id="tokens:187" class="idref" href="#tokens:187"><span class="id" title="binder">tokens</span></a> := <a class="idref" href="ImpParser.html#tokenize"><span class="id" title="definition">tokenize</span></a> <a class="idref" href="ImpParser.html#str:186"><span class="id" title="variable">str</span></a> <span class="id" title="keyword">in</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="ImpParser.html#parseSequencedCommand"><span class="id" title="definition">parseSequencedCommand</span></a> <a class="idref" href="ImpParser.html#bignumber"><span class="id" title="definition">bignumber</span></a> <a class="idref" href="ImpParser.html#tokens:187"><span class="id" title="variable">tokens</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">c</span><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Lists.List.html#ae9a5e1034e143b218b09d8e454472bd"><span class="id" title="notation">[]</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> ⇒ <a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <span class="id" title="var">c</span><br/>
&nbsp;&nbsp;| <a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">_</span><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a> <span class="id" title="var">t</span><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#::list_scope:x_'::'_x"><span class="id" title="notation">::</span></a><span class="id" title="var">_</span><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> ⇒ <a class="idref" href="ImpParser.html#NoneE"><span class="id" title="constructor">NoneE</span></a> ("Trailing tokens remaining: " <a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#169ad156fbc6036a53a0338819a2b301"><span class="id" title="notation">++</span></a> <span class="id" title="var">t</span>)<br/>
&nbsp;&nbsp;| <a class="idref" href="ImpParser.html#NoneE"><span class="id" title="constructor">NoneE</span></a> <span class="id" title="var">err</span> ⇒ <a class="idref" href="ImpParser.html#NoneE"><span class="id" title="constructor">NoneE</span></a> <span class="id" title="var">err</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
<a id="lab390"></a><h1 class="section">Examples</h1>

</div>
<div class="code">

<span class="id" title="keyword">Example</span> <a id="eg<sub>1</sub>" class="idref" href="#eg<sub>1</sub>"><span class="id" title="definition">eg<sub>1</sub></span></a> : <a class="idref" href="ImpParser.html#parse"><span class="id" title="definition">parse</span></a> "
  if x = y + 1 + 2 - y * 6 + 3 then
    x := x * 1;
    y := 0
  else
    skip
  end  "<br/>
<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <a class="idref" href="Imp.html#23430cd9e427d30c054d4f029e39cb7f"><span class="id" title="notation">&lt;{</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Imp.html#:com:com_scope:'if'_x_'then'_x_'else'_x_'end'"><span class="id" title="notation">if</span></a> <a class="idref" href="Imp.html#5a96623d056c293ebbcdf03005796e<sub>09</sub>"><span class="id" title="notation">(</span></a>"x" <a class="idref" href="Imp.html#9e5b22caf5d7cf490e97976162618c2a"><span class="id" title="notation">=</span></a> <a class="idref" href="Imp.html#5a96623d056c293ebbcdf03005796e<sub>09</sub>"><span class="id" title="notation">(</span></a>"y" <a class="idref" href="Imp.html#ad27fd091d9c8494ce7e5135135d19a<sub>8</sub>"><span class="id" title="notation">+</span></a> 1 <a class="idref" href="Imp.html#ad27fd091d9c8494ce7e5135135d19a<sub>8</sub>"><span class="id" title="notation">+</span></a> 2 <a class="idref" href="Imp.html#:com::x_'-'_x"><span class="id" title="notation">-</span></a> "y" <a class="idref" href="Imp.html#a73c7b35e67094dc8ae672f3a93da066"><span class="id" title="notation">×</span></a> 6 <a class="idref" href="Imp.html#ad27fd091d9c8494ce7e5135135d19a<sub>8</sub>"><span class="id" title="notation">+</span></a> 3<a class="idref" href="Imp.html#5a96623d056c293ebbcdf03005796e<sub>09</sub>"><span class="id" title="notation">))</span></a> <a class="idref" href="Imp.html#:com:com_scope:'if'_x_'then'_x_'else'_x_'end'"><span class="id" title="notation">then</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"x" <a class="idref" href="Imp.html#91e9aa710642047a93142bdf557f1a1b"><span class="id" title="notation">:=</span></a> "x" <a class="idref" href="Imp.html#a73c7b35e67094dc8ae672f3a93da066"><span class="id" title="notation">×</span></a> 1<a class="idref" href="Imp.html#313afe74ec81f2da17d8e7bca3b042e<sub>7</sub>"><span class="id" title="notation">;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"y" <a class="idref" href="Imp.html#91e9aa710642047a93142bdf557f1a1b"><span class="id" title="notation">:=</span></a> 0<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Imp.html#:com:com_scope:'if'_x_'then'_x_'else'_x_'end'"><span class="id" title="notation">else</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Imp.html#:com:com_scope:'skip'"><span class="id" title="notation">skip</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Imp.html#:com:com_scope:'if'_x_'then'_x_'else'_x_'end'"><span class="id" title="notation">end</span></a> <a class="idref" href="Imp.html#23430cd9e427d30c054d4f029e39cb7f"><span class="id" title="notation">}&gt;</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">cbv</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Example</span> <a id="eg<sub>2</sub>" class="idref" href="#eg<sub>2</sub>"><span class="id" title="definition">eg<sub>2</sub></span></a> : <a class="idref" href="ImpParser.html#parse"><span class="id" title="definition">parse</span></a> "
  skip;
  z:=x*y*(x*x);
  while x=x do
    if (z &lt;= z*z) &amp;&amp; ~(x = 2) then
      x := z;
      y := z
    else
      skip
    end;
    skip
  end;
  x:=z  "<br/>
<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="ImpParser.html#SomeE"><span class="id" title="constructor">SomeE</span></a> <a class="idref" href="Imp.html#23430cd9e427d30c054d4f029e39cb7f"><span class="id" title="notation">&lt;{</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Imp.html#:com:com_scope:'skip'"><span class="id" title="notation">skip</span></a><a class="idref" href="Imp.html#313afe74ec81f2da17d8e7bca3b042e<sub>7</sub>"><span class="id" title="notation">;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"z" <a class="idref" href="Imp.html#91e9aa710642047a93142bdf557f1a1b"><span class="id" title="notation">:=</span></a> "x" <a class="idref" href="Imp.html#a73c7b35e67094dc8ae672f3a93da066"><span class="id" title="notation">×</span></a> "y" <a class="idref" href="Imp.html#a73c7b35e67094dc8ae672f3a93da066"><span class="id" title="notation">×</span></a> <a class="idref" href="Imp.html#5a96623d056c293ebbcdf03005796e<sub>09</sub>"><span class="id" title="notation">(</span></a>"x" <a class="idref" href="Imp.html#a73c7b35e67094dc8ae672f3a93da066"><span class="id" title="notation">×</span></a> "x"<a class="idref" href="Imp.html#5a96623d056c293ebbcdf03005796e<sub>09</sub>"><span class="id" title="notation">)</span></a><a class="idref" href="Imp.html#313afe74ec81f2da17d8e7bca3b042e<sub>7</sub>"><span class="id" title="notation">;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Imp.html#:com:com_scope:'while'_x_'do'_x_'end'"><span class="id" title="notation">while</span></a> <a class="idref" href="Imp.html#5a96623d056c293ebbcdf03005796e<sub>09</sub>"><span class="id" title="notation">(</span></a>"x" <a class="idref" href="Imp.html#9e5b22caf5d7cf490e97976162618c2a"><span class="id" title="notation">=</span></a> "x"<a class="idref" href="Imp.html#5a96623d056c293ebbcdf03005796e<sub>09</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="Imp.html#:com:com_scope:'while'_x_'do'_x_'end'"><span class="id" title="notation">do</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Imp.html#:com:com_scope:'if'_x_'then'_x_'else'_x_'end'"><span class="id" title="notation">if</span></a> <a class="idref" href="Imp.html#5a96623d056c293ebbcdf03005796e<sub>09</sub>"><span class="id" title="notation">(</span></a>"z" <a class="idref" href="Imp.html#d43f15edd52d29ae8e0f90730a25ed5c"><span class="id" title="notation">≤</span></a> "z" <a class="idref" href="Imp.html#a73c7b35e67094dc8ae672f3a93da066"><span class="id" title="notation">×</span></a> "z"<a class="idref" href="Imp.html#5a96623d056c293ebbcdf03005796e<sub>09</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="Imp.html#:com::x_'&amp;&amp;'_x"><span class="id" title="notation">&amp;&amp;</span></a> <a class="idref" href="Imp.html#dfe50505b2b595242030c436d0d7d15f"><span class="id" title="notation">¬</span></a><a class="idref" href="Imp.html#5a96623d056c293ebbcdf03005796e<sub>09</sub>"><span class="id" title="notation">(</span></a>"x" <a class="idref" href="Imp.html#9e5b22caf5d7cf490e97976162618c2a"><span class="id" title="notation">=</span></a> 2<a class="idref" href="Imp.html#5a96623d056c293ebbcdf03005796e<sub>09</sub>"><span class="id" title="notation">)</span></a> <a class="idref" href="Imp.html#:com:com_scope:'if'_x_'then'_x_'else'_x_'end'"><span class="id" title="notation">then</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"x" <a class="idref" href="Imp.html#91e9aa710642047a93142bdf557f1a1b"><span class="id" title="notation">:=</span></a> "z"<a class="idref" href="Imp.html#313afe74ec81f2da17d8e7bca3b042e<sub>7</sub>"><span class="id" title="notation">;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"y" <a class="idref" href="Imp.html#91e9aa710642047a93142bdf557f1a1b"><span class="id" title="notation">:=</span></a> "z"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Imp.html#:com:com_scope:'if'_x_'then'_x_'else'_x_'end'"><span class="id" title="notation">else</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Imp.html#:com:com_scope:'skip'"><span class="id" title="notation">skip</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Imp.html#:com:com_scope:'if'_x_'then'_x_'else'_x_'end'"><span class="id" title="notation">end</span></a><a class="idref" href="Imp.html#313afe74ec81f2da17d8e7bca3b042e<sub>7</sub>"><span class="id" title="notation">;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Imp.html#:com:com_scope:'skip'"><span class="id" title="notation">skip</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Imp.html#:com:com_scope:'while'_x_'do'_x_'end'"><span class="id" title="notation">end</span></a><a class="idref" href="Imp.html#313afe74ec81f2da17d8e7bca3b042e<sub>7</sub>"><span class="id" title="notation">;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"x" <a class="idref" href="Imp.html#91e9aa710642047a93142bdf557f1a1b"><span class="id" title="notation">:=</span></a> "z" <a class="idref" href="Imp.html#23430cd9e427d30c054d4f029e39cb7f"><span class="id" title="notation">}&gt;</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">cbv</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;2021-08-11&nbsp;15:08&nbsp;*)</span><br/>
</div>
</div>

<div id="footer">
<hr/><a href="coqindex.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
</div>

</div>

</body>
</html>